『Sets in types, types in sets』
Werner, Benjamin. Sets in types, types in sets. 2006, p. 530–546, ISBN978-3-540-63388-4.
Title: Sets in Types, Types in Sets
Author: Benjamin Werner
Year: 2006
1. どんなもの？
2. 先行研究と比べてどこがすごい？
AczelやCoquandらによる既存の一方向的エンコードに対し、本論文は双方向のエンコードを構築し、さらに表現力の階層性とその関係を明示的に比較した点で新しい。また、Coqによる形式検証も行っている。
3. 技術や手法のキモはどこ？
CICをZFCにエンコードする際は、Coquandの証明無関係/証明非依存性（proof-irrelevance）意味論を拡張。 ZFCをCICにエンコードする際は、Aczelの帰納的集合構成法を採用。
型理論におけるuniversesの数と集合論における到達不能基数(inaccessible cardinal)の数を対応させている。 4. どうやって有効だと検証した？
CICからZFCへのエンコードの正当性は、証明無関係意味論に基づいた健全性定理で確認。 ZFCからCICへのエンコードは、Coqを用いて形式的に証明ファイルを作成して確認。 相対的一貫性定理を示すことで、論理的強度の比較と整合性の検証を行っている。
5. 議論はある？
型理論における選択公理（TTDA(型理論的記述公理)やTTCA(型理論的選択公理)）の要否や、より弱い公理での代替可能性が未解決問題。
非可述性(Impredicativity)の扱い、特に証明の抽出ができない点に関する制約や、それに対する構成的論理(constructive logic)との整合性も議論の対象。 到達不能基数の形式的構成も将来的課題として残る。
6. 次に読むべき論文は？
Peter Aczel (1977), "The Type Theoretic Interpretation of Constructive Set Theory"
→ 本論文のZFCからCICへのエンコードの技術的基盤を与えた代表的な先行研究。帰納的集合構成と構成的集合論の型理論的定式化を行っている。
Thierry Coquand and Christine Paulin-Mohring (1990), "Inductively defined types"
→ 帰納型の形式定義と、それが型理論においてどのように導入されるかを論じた基本文献。CICの基盤に位置付けられる。
Thomas Altenkirch (1993), "Constructions, Inductive Types and Strong Normalization"
→ 型理論の正規化証明におけるモデル構成法の技術的前進を提供。証明非依存性の意味論に基づくモデル構成の理解に寄与。
Benjamin Werner (1997), "An Encoding of ZFC Set Theory in Coq"
→ 本論文の技術実装にあたるCoqによるZFCの形式化ファイル。実践的な理解を深めるのに適している。
$ s = \text{Prop} \mid \text{Type}_i
この論文でのPropの型は$ [] \vdash \text{Prop : Type}_1 になっている
ZFCをCICの中(Coqで)書いたもの
table:訳
predicative universe 可述的宇宙 inductive type 帰納型
pure type system (pts) 純粋型体系(純粋型システム
proof-irrelevance 証明非依存性(証明無関係)
inaccessible cardinal 到達不能基数
lamda abstraction ラムダ抽象
axiom of choice 選択公理
extensionality 外延性
cumulativity 累積性
constructive logic 構成的論理
excluded middle 排中律
replacement schema 置換スキーマ
pair set 対集合
empty set 空集合
powerset 冪集合
comprehension scheme 内包スキーマ
intersection set 共通部分集合
natural numbers 自然数
type-theoretical description axiom (ttda) 型理論的記述公理（TTDA）
type-theoretical choice axiom (ttca) 型理論的選択公理（TTCA）
dependent type 依存型
curry-howard isomorphism カリー＝ハワード同型対応
martin-löf type theory マルティン＝レーフ型理論
strong normalization 強正規化
model construction モデル構成
normalization proof 正規化証明
propositional logic 命題論理
term 項
typing rule 型付け規則
substitution 置換
beta-reduction ベータ簡約
beta-conversion ベータ変換
positivity condition 正の位置制約
least fixed-point 最小不動点
monotone operator 単調作用素
recursive argument 再帰引数
logical strength 論理的強度
relative consistency 相対的一貫性
constructive ordinal 構成的順序数
logical framework 論理枠組み
formalization 形式化
set membership 集合の所属
structural recursion 構造的再帰
case analysis ケース分析
structural induction 構造的帰納法
functional predicate 関数的述語
syntax 構文
semantics 意味論
equivalence relation 同値関係
leibniz equality ライプニッツの等価性